T, S:Type, op:(STT). SqStable(Cancel(T;S;op)) 

latex

Up	gen algebra 1
Definitions of Statement	Cancel(T;S;op)
Definitions	x. t(x), t  T, , x f y, P  Q, Cancel(T;S;op), x:A. B(x), x(s)
Lemmas	sq stable equal, sq stable implies, sq stable all